ErdosProblems: add 71, 206, 209, 328, 353, 403, 426, 464, 512, 621, 639, 648 (#3998 sync)#4385
ErdosProblems: add 71, 206, 209, 328, 353, 403, 426, 464, 512, 621, 639, 648 (#3998 sync)#4385williamjblair wants to merge 5 commits into
Conversation
|
👋 This is an automated welcome message. 🤖 A few friendly reminders while the review gets started:
Thanks again for helping improve Formal Conjectures. |
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Thanks! Looks pretty good, just a few nits about moving stuff to FormalConjecturesForMathlib/re-using stuff from there...
| /-- All elements of the finset are positive (valid denominators). -/ | ||
| def ValidEgyptian (S : Finset ℕ) : Prop := | ||
| ∀ m ∈ S, 0 < m |
There was a problem hiding this comment.
potentially inline? It is only used once
|
|
||
| /-- The Egyptian fraction sum: `∑_{m ∈ S} 1/m` for a finset of natural numbers. -/ | ||
| noncomputable def egyptianSum (S : Finset ℕ) : ℝ := | ||
| S.sum (fun m => (1 : ℝ) / m) |
There was a problem hiding this comment.
| S.sum (fun m => (1 : ℝ) / m) | |
| ∑ m ∈ S, (1 : ℝ) / m |
better equivalent notation?
I feel like this should probably go into ForMathlib somewhere: isn't this uesd also in other problems?
| def IsLine (L : AffineSubspace ℝ ℝ²) : Prop := | ||
| ∃ p q : ℝ², p ≠ q ∧ L = affineSpan ℝ {p, q} |
There was a problem hiding this comment.
| def IsLine (L : AffineSubspace ℝ ℝ²) : Prop := | |
| ∃ p q : ℝ², p ≠ q ∧ L = affineSpan ℝ {p, q} | |
| def IsLine (L : AffineSubspace ℝ ℝ²) : Prop := | |
| finrank ℝ L.direction = 1 |
Would this be more mathlib idiomatic (untested).
Perhaps also good to either inline or move to ForMathlib?
| theorem erdos_353.variants.isosceles_triangle : | ||
| ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ → | ||
| ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, | ||
| (dist a b = dist a c ∨ dist b a = dist b c ∨ dist c a = dist c b) ∧ |
There was a problem hiding this comment.
re-use IsIsosceles from FormalConjecturesForMathlib/Geometry/2d.lean?
instead of inlining it here?
| theorem erdos_353.variants.right_angled_triangle : | ||
| ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ → | ||
| ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, | ||
| (∠ b a c = π / 2 ∨ ∠ a b c = π / 2 ∨ ∠ b c a = π / 2) ∧ |
There was a problem hiding this comment.
This should be factored out into a clean IsRightAngled definition in FormalConjecturesForMathlib/Geometry/2d.lean, if not there already
| parallel sides together with equal diagonals is the classical characterization of | ||
| an isosceles trapezoid; in particular it rules out non-rectangular parallelograms. | ||
| -/ | ||
| def IsIsoscelesTrapezoid (a b c d : ℝ²) : Prop := |
There was a problem hiding this comment.
belongs in FormalConjecturesForMathlib/Geometry/2d.lean as part of the standard 2D geometry API, where IsCcwConvexPolygon is also defined.
| /-- | ||
| `G` is a **unique subgraph** of `H` if there is exactly one subgraph of `H` isomorphic to `G`. | ||
| Subgraphs of `H` are taken in the spanning sense: elements `G' ≤ H` of the lattice | ||
| `SimpleGraph (Fin n)`, i.e. subsets of the edges of `H` (not necessarily induced). | ||
| -/ | ||
| def IsUniqueSubgraph {n : ℕ} (G H : SimpleGraph (Fin n)) : Prop := | ||
| ∃! G' : SimpleGraph (Fin n), G' ≤ H ∧ Nonempty (G.Iso G') | ||
|
|
||
| /-- | ||
| The number of distinct unique subgraphs of `H`: the number of isomorphism classes of graphs | ||
| that occur exactly once as a subgraph of `H`. Each such class contains exactly one subgraph | ||
| `G ≤ H` (uniqueness forbids a second isomorphic copy), so counting those representatives | ||
| counts the classes. | ||
| -/ | ||
| noncomputable def uniqueSubgraphCount {n : ℕ} (H : SimpleGraph (Fin n)) : ℕ := | ||
| {G : SimpleGraph (Fin n) | G ≤ H ∧ IsUniqueSubgraph G H}.ncard |
There was a problem hiding this comment.
probably best to create FormalConjecturesForMathlib/Combinatorics/SimpleGraph/SubgraphIsomorphism.lean. Move IsUniqueSubgraph and uniqueSubgraphCount there. Add @[category test] sanity checks.
| /-- Shorthand for the additive character $e(x) = e^{2\pi i x}$. -/ | ||
| noncomputable def e (x : ℝ) : ℂ := Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I) |
There was a problem hiding this comment.
This exact definition is duplicated across 512.lean, 987.lean, and appears in SpectralSets.lean as exponentialCharacter. While 987.lean notes it is kept local for readability, having def e copy-pasted in every analytic number theory seems silly. Consider moving def e into a suitable shared file in FormalConjecturesForMathlib.
mo271
added
the
awaiting-author
- 353: move IsIsoscelesTrapezoid into FormalConjecturesForMathlib/Geometry/2d.lean; reuse the existing IsIsosceles; add IsRightAngled there and use it - 206: use big-operator notation for egyptianSum; inline the single-use ValidEgyptian - 209: define IsLine via finrank of the direction (mo271's suggestion)
- 426: move IsUniqueSubgraph and uniqueSubgraphCount into a new
FormalConjecturesForMathlib/Combinatorics/SimpleGraph/SubgraphIsomorphism.lean
(generalized to any vertex type); add a @[category test] sanity check
- 512: extract the additive character e(x)=e^{2πix} into a shared
FormalConjecturesForMathlib/Analysis/SpecialFunctions/AdditiveCharacter.lean;
512 and 987 now reuse it instead of copy-pasting the definition
|
Thanks, should be all applied
|
2 participants
Adds Formal Conjectures statements for Erdős problems 71, 206, 209, 328, 353, 403, 426, 464, 512, 621, 639, 648.
Each statement was drafted from the boxed problem text on erdosproblems.com (docstrings verbatim), cross-checked against hosted Lean statements/proofs where available, and reviewed for statement fidelity before submission. No
formal_proofannotation is included in this batch; 648 has a nearby hosted proof, but this PR follows the problem-text range rather than the hosted range. Divergences from the hosted formalizations are noted below.¬ ∀ d, ...; we use the FC house form for disproved yes/no problems,answer(False) ↔ ∀ d, ...(logically equivalent, matches e.g. FC 1128).; …answer(False) <-> P(upstream state 'disproved (Lean)' maps to FC category 'research solved' with answer False, per the batch-3 429 precedent); …AddCircle (1 : ℝ)withhaarAddCircleand thefouriermonomials; we integrate over θ ∈ [0,1] withintervalIntegral, following the problem text's ∫_0^1 literally.; …Trigraphreformulation and proves inequalities between abstract quantities (P4, C4, D, K13) with no n^2/4 normalization and no alpha_1/tau_1 extremal values; …10 <= Fintype.card V; the draft instead uses the asymptotic formforall-eventually n in atTop(FC house style for 'sufficiently large', cf; …For 621, see also #835.
Part of #3998.